Search for: All records

Cloud systems are increasingly being managed by operation programs termed operators, which automate tedious, human-based operations. Operators of modern management platforms like Kubernetes, Twine, and ECS implement declarative interfaces based on the state-reconciliation principle. An operation declares a desired system state and the operator automatically reconciles the system to that declared state. Operator correctness is critical, given the impacts on system operations—bugs in operator code put systems in undesired or error states, with severe consequences. However, validating operator correctness is challenging due to the enormous system-state space and complex operation interface. A correct operator must not only satisfy correctness properties of its own code, but it must also maintain managed systems in desired states. Unfortunately, end-to-end testing of operators significantly falls short. We present Acto, the first automatic end-to-end testing technique for cloud system operators. Acto uses a statecentric approach to test an operator together with a managed system. Acto continuously instructs an operator to reconcile a system to different states and checks if the system successfully reaches those desired states. Acto models operations as state transitions and systematically realizes state-transition sequences to exercise supported operations in different scenarios. Acto’s oracles automatically check whether a system’s state is as desired. To date, Acto has helped find 56 serious new bugs (42 were confirmed and 30 have been fixed) in eleven Kubernetes operators with few false alarms. 

Graph-based intermediate representations (IRs) are widely used for powerful compiler optimizations, either interprocedurally in pure functional languages, or intraprocedurally in imperative languages. Yet so far, no suitable graph IR exists for aggressive global optimizations in languages with both effects and higher-order functions: aliasing and indirect control transfers make it difficult to maintain sufficiently granular dependency information for optimizations to be effective. To close this long-standing gap, we propose a novel typed graph IR combining a notion of reachability types with an expressive effect system to compute precise and granular effect dependencies at an affordable cost while supporting local reasoning and separate compilation. Our high-level graph IR imposes lexical structure to represent structured control flow and nesting, enabling aggressive and yet inexpensive code motion and other optimizations for impure higher-order programs. We formalize the new graph IR based on a λ-calculus with a reachability type-and-effect system along with a specification of various optimizations. We present performance case studies for tensor loop fusion, CUDA kernel fusion, symbolic execution of LLVM IR, and SQL query compilation in the Scala LMS compiler framework using the new graph IR. We observe significant speedups of up to 21x.

 

Realizing a large Landég-factor of electrons in solid-state materials has long been thought of as a rewarding task as it can trigger abundant immediate applications in spintronics and quantum computing. Here, by using metamorphic InAsSb/InSb superlattices (SLs), we demonstrate an unprecedented high value ofg≈ 104, twice larger than that in bulk InSb, and fully spin-polarized states at low magnetic fields. In addition, we show that theg-factor can be tuned on demand from 20 to 110 via varying the SL period. The key ingredients of such a wide tunability are the wavefunction mixing and overlap between the electron and hole states, which have drawn little attention in prior studies. Our work not only establishes metamorphic InAsSb/InSb as a promising and competitive material platform for future quantum devices but also provides a new route towardg-factor engineering in semiconductor structures.

 

Ownership type systems, based on the idea of enforcing unique access paths, have been primarily focused on objects and top-level classes. However, existing models do not as readily reflect the finer aspects of nested lexical scopes, capturing, or escaping closures in higher-order functional programming patterns, which are increasingly adopted even in mainstream object-oriented languages. We present a new type system, λ * , which enables expressive ownership-style reasoning across higher-order functions. It tracks sharing and separation through reachability sets, and layers additional mechanisms for selectively enforcing uniqueness on top of it. Based on reachability sets, we extend the type system with an expressive flow-sensitive effect system, which enables flavors of move semantics and ownership transfer. In addition, we present several case studies and extensions, including applications to capabilities for algebraic effects, one-shot continuations, and safe parallelization. 

The identification of a non-trivial band topology usually relies on directly probing the protected surface/edge states. But, it is difficult to achieve electronically in narrow-gap topological materials due to the small (meV) energy scales. Here, we demonstrate that band inversion, a crucial ingredient of the non-trivial band topology, can serve as an alternative, experimentally accessible indicator. We show that an inverted band can lead to a four-fold splitting of the non-zero Landau levels, contrasting the two-fold splitting (spin splitting only) in the normal band. We confirm our predictions in magneto-transport experiments on a narrow-gap strong topological insulator, zirconium pentatelluride (ZrTe₅), with the observation of additional splittings in the quantum oscillations and also an anomalous peak in the extreme quantum limit. Our work establishes an effective strategy for identifying the band inversion as well as the associated topological phases for future topological materials research.